The proofs operate entirely within the quantifier-free bitvector (QF_BV)
logic, so there is no need to use the generic solver.

This updates `prove` to construct a QF_BV solver that is specialized for
the logic being proved directly which avoids the overhead of selecting
from more general solving strategies.

This makes use of BitVecVals to specify multiple vectors at the same
time which both improves readability and makes the proofs slightly more
compact.  It also makes the field64 reducer proof more closely match the
source code which accesses the limb of x by array index.

The existing formal proof for the 4x64 field reduction establishes the
intermediate bounds and verifies that no carries are discarded.

This extends it to include a full end-to-end functional correctness
proof that shows the implementation computes the correct reduction
modulo the field prime for all 512-bit inputs.

This updates the README.md and doc.go files to include some important
caveats about the constant time and memory clearing behavior.
Specifically, while the behavior has been manually verified by carefully
reviewing the generated assembly as of the most recent version of Go, it
is impossible to guarantee the compiler will not change in the future.

This adds a new test helper for some algebraic properties of scalar
negation and calls it from the test that handles specific edge cases as
well as the randomized test.

This adds a new test helper for some algebraic properties of modular
multiplicative inverses of scalars and calls it from the test that
handles specific edge cases as well as the randomized test.

This adds a new test helper for some algebraic properties of the scalar
half order check and calls it from the test that handles specific edge
cases as well as the randomized test.

This significantly optimizes the ModNScalar implementation by rewriting
it to use saturated 4x64 arithmetic similar to the new 4x64 field
arithmetic.

The new implementation retains all of the important properties such as
being constant time and only using temporary buffers on the stack that
are cleared.

Of particular interest is the new modular reduction implementation.  It
moves away from the 96-bit accumulate design and instead manually tracks
and discards carries inline which provides a major speed advantage.

Due to the complexity and potential mistakes in the arithmetic, all of
the intermediate bounds and carry assumptions documented that the code
relies upon have been formally verified to be correct.  The formal proof
is in a separate commit.

The implementation is primarily targeted at 64-bit since it is by far
the most common architecture in modern use, however, as the included
benchmarks below show, it is faster for almost all operations on 32-bit
architectures as well.  The few operations where it is a bit slower on
32-bit architectures are not used anywhere near as frequently as the
ones that get 10-30% better performance, so the end result is the
overall implementation is notably faster on 32 bit too.

For 64-bit architectures, every operation is significantly faster.  For
example, all of the primary operations that get heavy use get ~73-94%
better performance.

Finally, the tests have been updated to use values specifically crafted
to exercise the new limbs versus the old values that were crafted for
the old limbs.

Comparison for 32-bit platforms:

$ benchstat beforescalar_x86.txt afterscalar_x86.txt
name                          old time/op    new time/op    delta
-----------------------------------------------------------------------------------
ModNScalar                  22.9ns ± 4%    23.2ns ± 5%      ~ (p=0.184 n=10+10)
ModNScalarZero              1.36ns ± 3%    6.59ns ± 6%  +385.95% (p=0.000 n=9+9)
ModNScalarIsZero            0.32ns ± 4%    0.34ns ±14%      ~ (p=0.143 n=10+10)
ModNScalarEquals            3.69ns ± 4%    0.30ns ± 7%   -91.78% (p=0.000 n=10+10)
ModNScalarAdd               25.1ns ± 6%    22.5ns ± 5%   -10.40% (p=0.000 n=9+10)
ModNScalarMul                257ns ± 5%     223ns ± 5%   -13.07% (p=0.000 n=10+10)
ModNScalarSquare             267ns ± 5%     172ns ± 6%   -35.56% (p=0.000 n=10+10)
ModNScalarNegate            12.8ns ± 9%    14.5ns ± 2%   +13.39% (p=0.000 n=10+10)
ModNScalarInverse            686ns ± 7%     623ns ± 3%    -9.24% (p=0.000 n=10+9)
ModNScalarIsOverHalfOrder   8.92ns ± 6%    6.55ns ± 3%   -26.59% (p=0.000 n=10+10)

Comparison for 64-bit platforms:

$ benchstat beforescalar_x64.txt afterscalar_x64.txt
name                          old time/op    new time/op    delta
ModNScalar                   12.1ns ± 1%     3.5ns ± 4%  -71.25% (p=0.000 n=7+10)
ModNScalarZero               0.64ns ± 9%    0.61ns ± 5%   -4.08% (p=0.043 n=10+10)
ModNScalarIsZero             0.31ns ± 8%    0.31ns ± 6%      ~   (p=0.000 n=10+10)
ModNScalarEquals             2.63ns ± 5%    0.33ns ± 9%  -87.47% (p=0.000 n=10+10)
ModNScalarAdd                15.1ns ± 4%     4.1ns ± 4%  -73.25% (p=0.000 n=10+10)
ModNScalarMul                 214ns ± 6%      29ns ± 6%  -86.30% (p=0.000 n=10+10)
ModNScalarSquare              215ns ± 4%      23ns ± 6%  -89.39% (p=0.000 n=10+10)
ModNScalarNegate             5.78ns ± 4%    2.99ns ±10%  -48.33% (p=0.000 n=10+10)
ModNScalarInverse             452ns ± 4%     408ns ± 6%   -9.89% (p=0.000 n=10+10)
ModNScalarIsOverHalfOrder    5.52ns ± 6%    0.29ns ± 5%  -94.66% (p=0.000 n=10+9)

This adds a formal verification proof of the scalar reduction arithmetic
in the new 4x64 scalar implementation and updates the proofs README.md
accordingly.

It includes a formal proof for the following:

- 512-bit modular reduction over the group order with saturated 64-bit
  limbs

With the ultimate goal of optimizing scalar multiplication by reducing
the average number of point additions, this commit adds code to convert
a balanced scalar representative into width-5 windowed non-adjacent form
(wNAF).

The current scalar multiplication implementation uses ordinary
non-adjacent form (NAF), which corresponds to a window width of 2.

This commit introduces only the width-5 wNAF recoder and does not yet
integrate it into scalar multiplication.

Future commits will add comprehensive tests and integrate the new
implementation.

This adds comprehensive tests for the new wNAF implementation to help
verify correctness.

The tests assert the resulting encoding satisfies the required
mathematical properties and reconstructs the original value for both
deterministic edge cases and randomized balanced scalar representatives.

The deterministic edge cases exercise enough small values to
exhaustively test every residue modulo 2^w multiple times, and include
additional edge cases such as carries introduced by the recoding,
maximum values, and alternating bit patterns.

This updates the non-constant-time scalar multiplication implementation
to use the new width-5 wNAF recoding.

In particular, because wNAF requires precomputed odd multiples that were
not needed by the previous implementation, this introduces a new
dedicated precomputed table type along with a new helper to construct
the required multiples.

The previous implementation only needed to swap between two precomputed
points depending on the scalar signs.  However, since the new wNAF
implementation uses larger precomputed tables, it instead tracks whether
each decomposed scalar was negated and applies the corresponding sign
adjustment to the appropriate half of each table.

The following benchmark shows a before and after comparison of scalar
multiplication:

name                 old time/op   new time/op   delta
---------------------------------------------------------------------------
ScalarMultNonConst   94.4µs ± 1%   84.3µs ± 1%   -10.75%  (p=0.000 n=10+10)

This removes the old ordinary NAF implementation that is no longer used
now that the implementation has been updated to use a new width-5 wNAF
recoder instead.

It also removes the associated tests and benchmark accordingly.